(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const v7 Bool)
(assert (exists ((q0 Bool) (q1 Bool) (q2 Int)) v2))
(declare-const v8 Bool)
(declare-const i4 Int)
(declare-const i5 Int)
(assert (not (exists ((q3 Int) (q4 Bool) (q5 Bool)) (not (and (<= 50 20) v4 q5 v6 v5 q4)))))
(declare-const v9 Bool)
(assert (not (exists ((q6 Int)) (not (<= i4 20)))))
(declare-const v10 Bool)
(assert (not (exists ((q7 Int)) (not (distinct q7 i5)))))
(assert (exists ((q8 Bool) (q9 Bool) (q10 Bool) (q11 Int)) (=> (distinct q11 919) (distinct q9 v7 q10 q9 (xor v1 v2 v4 v9 v5 v6 v0 v10) q10 v4))))
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const i6 Int)
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (or (and v6 (<= 50 20) (<= 50 20) v5 v1) v14 (and v14 v7 v10 v6 v6 (<= 50 20))))
(assert (or (and v14 v7 v10 v6 v6 (<= 50 20)) (distinct v5 v2 v9 v6 (<= 50 20) v5 (and v14 v7 v10 v6 v6 (<= 50 20)) v4 (= (- (mod 50 i3)) 919) v0 v8) v14))
(assert (or (and v14 v7 v10 v6 v6 (<= 50 20)) (and v14 v7 v10 v6 v6 (<= 50 20)) (<= 50 20)))
(assert (or (and v14 v7 v10 v6 v6 (<= 50 20)) (and v14 v7 v10 v6 v6 (<= 50 20)) (and v6 (<= 50 20) (<= 50 20) v5 v1)))
(assert (or (distinct v5 v2 v9 v6 (<= 50 20) v5 (and v14 v7 v10 v6 v6 (<= 50 20)) v4 (= (- (mod 50 i3)) 919) v0 v8) (and v14 v7 v10 v6 v6 (<= 50 20)) v14))
(check-sat)
